﻿// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==
using System;
using System.Collections.Generic;
using System.Text;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.ExtendedReflection.Collections;
using Microsoft.ExtendedReflection.Metadata;
using Microsoft.ExtendedReflection.Reasoning.ExecutionNodes;
using Microsoft.ExtendedReflection.Logging;
using Microsoft.ExtendedReflection.Utilities;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.ExtendedReflection.Utilities.Safe.Text;
using Microsoft.Pex.Fitness.Interfaces;

namespace Microsoft.Pex.Fitness.Implementation
{
    internal class PexFitnessExplorationManager
        : PexExplorationComponentBase
        , IPexFitnessExplorationManager
    {
        private readonly bool isLoggingEnabled;
        public bool IsLoggingEnabled
        {
            get { return this.isLoggingEnabled; }
        }

        private readonly bool useBranchFitnessGain;
        public bool UseBranchFitnessGain
        {
            get { return this.useBranchFitnessGain; }
        }

        private readonly bool isLoggingVerboseEnabled;
        public bool IsLoggingVerboseEnabled
        {
            get { return this.isLoggingVerboseEnabled; }
        }

        //which strategy to use in frontier
        private readonly PexFitnessStrategyKind strategy = PexFitnessStrategyKind.AlternateForTargets;

        //mapping from target id -> a set of node ids that include fitness values for the target id            
        private readonly SafeIntDictionary<SafeSet<int>> targetNodeMap = new SafeIntDictionary<SafeSet<int>>();

        //mapping from node id -> target-fitness info
        private readonly SafeIntDictionary<TargetFitnessInfo> nodeFitnessMap = new SafeIntDictionary<TargetFitnessInfo>();

        //a set of already covered targets
        private SafeSet<int> _coveredTargets;

        public bool HasCoveredTarget(int target)
        {
            return
                this._coveredTargets != null &&
                this._coveredTargets.Contains(target);
        }

        public void AddCoveredTarget(int target)
        {
            if (this._coveredTargets == null)
                this._coveredTargets = new SafeSet<int>();
            this._coveredTargets.Add(target);
        }

        //mapping from target id -> a set of branch ids that include fitness gains for the target id
        //this map is used when a target is covered and we need to update the branches' information
        private readonly SafeIntDictionary<SafeSet<int>> targetBranchMap = new SafeIntDictionary<SafeSet<int>>();

        //mapping from target id -> the best fitness value observed so far
        //this map is used to observe whether a certain run improves fitness values of at least one target
        //so that the frontier can reward such targets
        private readonly SafeIntDictionary<int> targetBestFitnessMap = new SafeIntDictionary<int>();

        //mapping from branch id -> the fitness gain if it is flipped
        readonly SafeIntDictionary<BranchFitnessGain> branchFitnessMap = new SafeIntDictionary<BranchFitnessGain>();

#if DEBUG
        //mapping from branch id -> branch label, debugging use
        private readonly SafeIntDictionary<string> branchIDMap = new SafeIntDictionary<string>();

        //mapping from target id -> target label, debugging use
        private readonly SafeIntDictionary<string> targetIDMap = new SafeIntDictionary<string>();
        public SafeIntDictionary<string> TargetIDMap
        {
            get { return this.targetIDMap; }
        }

        int currentPathNumber;
        public int CurrentPathNumber
        {
            get { return this.currentPathNumber; }
        }
        public void NextPathNumber()
        {
            this.currentPathNumber++;
        }

        //the info below is to keep track of info for the current run due to the preceding selected frontier node
        //debugging use
        private int TargetIDOfPrecedingFrontier = 0;
        private int FitnessValueOfPrecedingFrontier = int.MaxValue;
        private int PriorityOfTheChosenTargetInFrontier = int.MaxValue;

        public void SetSelectedFrontierInfo(int targetID, int fitnessValue, int priority)
        {
            TargetIDOfPrecedingFrontier = targetID;
            FitnessValueOfPrecedingFrontier = fitnessValue;
            PriorityOfTheChosenTargetInFrontier = priority;
        }
#endif

        public PexFitnessExplorationManager(
            PexFitnessStrategyKind strategy, 
            bool loggingEnabled, 
            bool isLoggingVerboseEnabled,
            bool useBranchFitnessGain)
        {
            this.strategy = strategy;
            this.isLoggingEnabled = loggingEnabled;
            this.isLoggingVerboseEnabled = isLoggingVerboseEnabled;
            this.useBranchFitnessGain = useBranchFitnessGain;
        }

        #region user priority methods
        //We use targetHashMethods to know the method that a target ID belongs to
        //The info is used when we allow a user-defined priority for a method
        //Then we can propogate the user-defined priority to the targets included in the method
        //mapping from target ID --> method definition
        SafeIntDictionary<SafeSet<MethodDefinition>> targetHashMethods = new SafeIntDictionary<SafeSet<MethodDefinition>>();

        public int GetTargetHash(ICallStackTrace callStackTrace, MethodDefinition method, int programCounter, bool taken)
        {
            // ignore callstack; didn't lead to good results;
            // (possible explanation: we wouldn't "learn" which branches are good in general, but it would have to be re-learned for every context)
            int res = HashCodeHelper.Combine(method.GlobalIndex, programCounter, (taken ? 1 : 0));
            SafeSet<MethodDefinition> s;
            if (!this.targetHashMethods.TryGetValue(res, out s))
                this.targetHashMethods[res] = s = new SafeSet<MethodDefinition>();
            s.Add(method);
            return res;
        }

        public IFiniteSet<MethodDefinition> GetMethodsOfTargetHash(int target)
        {
            SafeSet<MethodDefinition> s;
            if (this.targetHashMethods.TryGetValue(target, out s))
                return s;
            else
                return Set.Empty<MethodDefinition>();
        }

        SafeIntDictionary<int> methodDefinitionUserPriorities = new SafeIntDictionary<int>();
        public void SetUserPriority(MethodDefinition method, int priority)
        {
            SafeDebug.AssumeNotNull(method, "method");
            this.methodDefinitionUserPriorities[method.GlobalIndex] = priority;
            //this.Log.LogMessage("fitness", "Set {0} a user priority: {1}", method.ShortName, priority);
        }

        public bool TryGetUserPriority(MethodDefinition method, out int priority)
        {
            SafeDebug.AssumeNotNull(method, "method");
            return this.methodDefinitionUserPriorities.TryGetValue(method.GlobalIndex, out priority);
        }

        #endregion

        //target fitness info for each node
        class TargetFitnessInfo
        {
            PexFitnessExplorationManager owner;

            //mapping from targetID --> composite fitness value
            private readonly SafeIntDictionary<PexCompositeFitnessValue> targetCompositeFitnessMap = new SafeIntDictionary<PexCompositeFitnessValue>();
            public IFiniteMap<int, PexCompositeFitnessValue> TargetCompositeFitnessMap
            {
                get { return this.targetCompositeFitnessMap; }
            }

            public const int DefaultMinPexCompositeFitnessValue = int.MaxValue;

            //min fitness values among all targets' fitness values
            //this info is not used when we use the strategy of AlternateForTargets 
            //but used only for OverallMinFitnessValueForAllTargets
            //note that for the moment we still compute it even if it is not used in AlternateForTargets
            private int minPexCompositeFitnessValue = DefaultMinPexCompositeFitnessValue;
            public int MinPexCompositeFitnessValue
            {
                get { return this.minPexCompositeFitnessValue; }
            }

            //Node ID that this target fitness info belongs to
            //A link to point back the nodeID used in nodeFitness to map to this TargetFitness object
            private readonly int nodeID;

            //The physical branch that this node corresponds to so that we can calculate fitness gain/loss
            private int branchID;
            public int BranchID
            {
                get { return this.branchID; }
            }

            //targets covered by executing a branch of this node, debugging use
            private SafeSet<int> _coveredTargets;
            public IFiniteSet<int> CoveredTargets
            {
                get
                {
                    if (this._coveredTargets == null)
                        return Set.Empty<int>();
                    else
                        return this._coveredTargets;
                }
            }

#if DEBUG
            //the info below is to keep track of info for the node
            //debugging use
            public int firstEncounteredPathNumber = 0;//during which run/path, the current node is first created
            public int flippedPathNumber = 0;//during which run/path, the current node is last flipped
            public int TargetIDOfFlipping = 0;//for which target ID selected in the frontiers, the current node is last flipped
            public int FitnessValueOfFlipping = int.MaxValue;//for what fitness value of the target ID selected in the frontiers, the current node is last flipped
            public int PriorityOfTargetOfFlipping = int.MaxValue;//for what priority of the target ID selected in the frontiers, the current node is last flipped
            SafeIntDictionary<int> _fitnessGainForTargetOfFlipping; // target id -> fitness gain or loss when the current node is last flipped
            public IFiniteMap<int, int> FitnessGainForTargetOfFlipping
            {
                get
                {
                    if (this._fitnessGainForTargetOfFlipping == null)
                        return Map.Empty<int, int>();
                    else
                        return this._fitnessGainForTargetOfFlipping;
                }
            }
#endif

            public TargetFitnessInfo(
                PexFitnessExplorationManager owner,
                int nodeID)
            {
                this.nodeID = nodeID;
                this.branchID = int.MaxValue;
                this.owner = owner;
#if DEBUG
                this.firstEncounteredPathNumber = owner.currentPathNumber;
#endif
            }

#if DEBUG
            public void SetFlippedRunNumber(int pathNumber, int targetID, int fitnessValue, int targetPriority)
            {
                flippedPathNumber = pathNumber;
                TargetIDOfFlipping = targetID;
                FitnessValueOfFlipping = fitnessValue;
                PriorityOfTargetOfFlipping = targetPriority;
            }

            public void SetFitnessGainForCurrentNodeFlipping(int targetID, int fitnessValueGain)
            {
                if (this._fitnessGainForTargetOfFlipping == null)
                    this._fitnessGainForTargetOfFlipping = new SafeIntDictionary<int>();

                int oldFitnessGain;
                if (!this._fitnessGainForTargetOfFlipping.TryGetValue(targetID, out oldFitnessGain))
                    this._fitnessGainForTargetOfFlipping.Add(targetID, fitnessValueGain);
                else if (fitnessValueGain > oldFitnessGain)
                    this._fitnessGainForTargetOfFlipping[targetID] = fitnessValueGain;
            }
#endif

            public void AddCoveratedTargets(int targetID)
            {
                if (this._coveredTargets == null)
                    this._coveredTargets = new SafeSet<int>();
                this._coveredTargets.Add(targetID);
            }

            public void removeFitnessValueAfterTargetCoverage(int targetID)
            {
                PexCompositeFitnessValue PexCompositeFitnessValue;
                if (this.targetCompositeFitnessMap.TryGetValue(targetID, out PexCompositeFitnessValue))
                {
                    this.targetCompositeFitnessMap.Remove(targetID);

                    if (this.owner.strategy == PexFitnessStrategyKind.OverallMinFitnessValueForAllTargets)
                    {
                        int usedfitnessValue = PexCompositeFitnessValue.FitnessValue;
                        if (this.owner.UseBranchFitnessGain)
                            usedfitnessValue -= PexCompositeFitnessValue.BranchFitnessGain;
                        if (usedfitnessValue == this.minPexCompositeFitnessValue)
                        {
                            //need to find the existing min value after the targetID's fitness value is removed
                            var PexCompositeFitnessValueSet = this.targetCompositeFitnessMap.Values;
                            this.minPexCompositeFitnessValue = int.MaxValue;
                            foreach (var value in PexCompositeFitnessValueSet)
                            {
                                int compositeValue = value.FitnessValue;
                                if (this.owner.UseBranchFitnessGain)
                                    compositeValue -= value.BranchFitnessGain;
                                if (compositeValue < this.minPexCompositeFitnessValue)
                                    this.minPexCompositeFitnessValue = compositeValue;
                            }
                        }
                    }
                }
            }

            public int GetComputedFitness(int targetID)
            {
                PexCompositeFitnessValue PexCompositeFitnessValue;
                if (!this.TargetCompositeFitnessMap.TryGetValue(targetID, out PexCompositeFitnessValue))
                    return int.MaxValue;
                else
                {
                    int usedfitnessValue = PexCompositeFitnessValue.FitnessValue;
                    if (this.owner.UseBranchFitnessGain)
                        usedfitnessValue -= PexCompositeFitnessValue.BranchFitnessGain;
                    return usedfitnessValue;
                }
            }

            public int GetFitnessValue(int targetID)
            {
                PexCompositeFitnessValue PexCompositeFitnessValue;
                if (!this.TargetCompositeFitnessMap.TryGetValue(targetID, out PexCompositeFitnessValue))
                    return int.MaxValue;
                else
                {
                    return PexCompositeFitnessValue.FitnessValue;
                }
            }

            public void SetFitnessValue(int targetID, int fitnessValue, SafeIntDictionary<SafeSet<int>> targetNodeMap, int branchFitnessGain, int branchID)
            {
                if (this.targetCompositeFitnessMap.ContainsKey(targetID))
                {
                    this.targetCompositeFitnessMap[targetID] = new PexCompositeFitnessValue(fitnessValue, branchFitnessGain);
                }
                else
                {
                    PexCompositeFitnessValue PexCompositeFitnessValue = new PexCompositeFitnessValue(fitnessValue, branchFitnessGain);
                    this.targetCompositeFitnessMap.Add(targetID, PexCompositeFitnessValue);

                    //we next add the associated mapping from nodeID to targetID to targetNodeMap
                    //so that later when we cover a target, we can easily track down to the relevant nodeID
                    //for removing the entry of the target's fitness values
                    SafeSet<int> nodeIDSet;
                    if (!targetNodeMap.TryGetValue(targetID, out nodeIDSet))
                    {
                        targetNodeMap[targetID] = nodeIDSet = new SafeSet<int>();
                    }
                    nodeIDSet.Add(nodeID);
                }
                this.branchID = branchID;

                if (this.owner.strategy == PexFitnessStrategyKind.OverallMinFitnessValueForAllTargets)
                {
                    int usedFitnessValue = fitnessValue;
                    if (this.owner.UseBranchFitnessGain)
                        usedFitnessValue -= branchFitnessGain;
                    if (usedFitnessValue < this.minPexCompositeFitnessValue)
                        this.minPexCompositeFitnessValue = usedFitnessValue;
                }
            }
        }

        //(target -> fitness gain info) for each physical branch
        public class BranchFitnessGain
        {
            //fitness gain info for each physical branch w.r.t. a target
            struct FitnessGainInfo
            {
                public long AccumulatedBranchFitnessGain;
                public int Count;
            }

            //mapping from targetID --> fitness gain 
            private readonly SafeIntDictionary<FitnessGainInfo> branchFitnessGainMap = new SafeIntDictionary<FitnessGainInfo>();

            //Branch ID that this fitness gain info belongs to
            public readonly int BranchID; //a link to point back the branch used in locationFitness to map to this TargetFitnessGain object

            public BranchFitnessGain(int branchID)
            {
                this.BranchID = branchID;
            }

            public void RemoveFitnessGainAfterTargetCoverage(int branchID)
            {
                this.branchFitnessGainMap.Remove(branchID);
            }

            public int GetAverageFitnessGain(int branchID)
            {
                FitnessGainInfo fitnessGain;
                if (this.branchFitnessGainMap.TryGetValue(branchID, out fitnessGain))
                {
                    int count = fitnessGain.Count;
                    if (count > 0)
                    {
                        double relativeAccumulatedBranchFitnessGain = (double)fitnessGain.AccumulatedBranchFitnessGain / count;
                        if (fitnessGain.AccumulatedBranchFitnessGain > 0)
                            return (int)Math.Ceiling(relativeAccumulatedBranchFitnessGain);
                        else
                            return (int)Math.Floor(relativeAccumulatedBranchFitnessGain);
                    }
                    else
                        return 0;
                }
                else
                    return 0;
            }

            public long GetAccumulatedFitnessGain(int branchID)
            {
                FitnessGainInfo fitnessGain;
                if (this.branchFitnessGainMap.TryGetValue(branchID, out fitnessGain))
                    return fitnessGain.AccumulatedBranchFitnessGain;
                else
                    return 0;
            }

            public int GetAccumulatedFitnessCount(int branchID)
            {
                FitnessGainInfo fitnessGain;
                if (this.branchFitnessGainMap.TryGetValue(branchID, out fitnessGain))
                    return fitnessGain.Count;
                else
                    return 0;
            }

            public void AddFitnessGain(int branchID, int fitnessGainValue)
            {
                FitnessGainInfo fitnessGain;
                if (!this.branchFitnessGainMap.TryGetValue(branchID, out fitnessGain))
                    fitnessGain = new FitnessGainInfo();

                fitnessGain.AccumulatedBranchFitnessGain += -fitnessGainValue;
                fitnessGain.Count++;
                this.branchFitnessGainMap[branchID] = fitnessGain;
            }
        }

        #region other members of ExplorationMonitor

        void updateGlobalFitnessForTarget(SafeSet<int> targetsImprovedInThisPath, IExecutionNode flippedNode, int targetID, int fitnessValue)
        {
            int oldBestFitnessValue;
            if (!targetBestFitnessMap.TryGetValue(targetID, out oldBestFitnessValue))
            {
                targetBestFitnessMap.Add(targetID, fitnessValue);
            }
            else
            {
                if (fitnessValue < oldBestFitnessValue)
                {
                    targetBestFitnessMap[targetID] = fitnessValue;

                    if (targetsImprovedInThisPath.Add(targetID))
                    {
                        //below we notify the frontiers that the target ID has an improved fitness value
                        //so that reward can be given the target ID in the frontiers
                        RemoteEventHandler<PexFitnessEventArgs> eh2 = this.OnTargetFitnessImprovement;
                        if (eh2 != null)
                            eh2(new PexFitnessEventArgs(flippedNode, null, targetID));
                    }
                    /*!!*/if (this.IsLoggingEnabled)
                    this.Log.LogMessage("fitness", "global fitness of {0} set to {1}", targetID, fitnessValue);
                }
            }
        }

        //being invoked when a node is removed from the search frontiers
        //currently not used, since removing info may make things not working
        void removeNode(IExecutionNode node)
        {
            TargetFitnessInfo targetFitness;
            int nodeID = node.UniqueIndex;
            if (nodeFitnessMap.TryGetValue(nodeID, out targetFitness))
            {
                IFiniteMap<int, PexCompositeFitnessValue> targetFitnessMap = targetFitness.TargetCompositeFitnessMap;
                foreach (var targetID in Map.GetKeys(targetFitnessMap))
                {
                    SafeSet<int> nodeIDSet;
                    if (targetNodeMap.TryGetValue(targetID, out nodeIDSet))
                    {
                        nodeIDSet.Remove(nodeID);
                    }
                }
                nodeFitnessMap.Remove(nodeID);
            }
        }

        //being invoked when a target is covered
        //currently not used guarded by keepAlreadyCoveredTargetOrBranchFitnessForDebug
        //since removing info may lose debugging info
        public void RemoveFitnessAfterTargetCoverage(int targetID)
        {
            SafeSet<int> nodeIDSet;
            if (targetNodeMap.TryGetValue(targetID, out nodeIDSet))
            {
                foreach (var nodeID in nodeIDSet)
                {
                    TargetFitnessInfo targetFitness;
                    if (nodeFitnessMap.TryGetValue(nodeID, out targetFitness))
                        targetFitness.removeFitnessValueAfterTargetCoverage(targetID);
                }
                targetNodeMap.Remove(targetID);
            }
        }

        //being invoked when a target is covered
        //currently not used guarded by keepAlreadyCoveredTargetOrBranchFitnessForDebug
        //since removing info may lose debugging info
        public void RemoveFitnessGainAfterTargetCoverage(int targetID)
        {
            SafeSet<int> branchIDSet;
            if (targetBranchMap.TryGetValue(targetID, out branchIDSet))
            {
                foreach (var branchID in branchIDSet)
                {
                    BranchFitnessGain targetFitnessGain;
                    if (branchFitnessMap.TryGetValue(branchID, out targetFitnessGain))
                        targetFitnessGain.RemoveFitnessGainAfterTargetCoverage(targetID);
                }
                targetBranchMap.Remove(targetID);
            }
        }

        public void SetFitness(
            SafeSet<int> targetsImprovedInThisPath, 
            IExecutionNode flippedNode, 
            IEnumerable<IExecutionNode> reversePath,
            int targetID, int pathFitnessValue)
        {
            IExecutionNode lastVisitedNode = null; // note that we are going backwards
            foreach (IExecutionNode node in reversePath)
            {
                SafeDebug.Assert(
                    lastVisitedNode == null ||
                    Set.Enumerable(null, Map.GetValues(node.Successors)).Contains(lastVisitedNode),
                    "nodes must be in reverse order");

                BranchFitnessGain cli;
                BranchFitnessGain cliFlipFrom;
                int branchIDForCli;
                int branchIDForcliFlipFrom;
                CodeBranch branch;
                if (lastVisitedNode != null)
                    branch = lastVisitedNode.InCodeBranch;
                else
                {
                    //this is the first node, i.e., the current node of the target branching node
                    //we use the first branch of the current node to approximate
                    //nikolait: The following will not work when this node is part of the path suffix that we haven't seen yet ever
                    branch = Enumerable.FirstOrDefault<CodeBranch>(node.OutCodeBranches);

                    //currently the flipping of predicates/branches involving symbolic values has
                    //been implemented at the end of the path and traversing back the nodes int the path
                    //See PathMonitor.OnPathFinished()
                }

                if (branch != null)
                {
                    int methodIDFlip = 0;
                    if (branch.Method != null)
                        methodIDFlip = branch.Method.GlobalIndex;

                    branchIDForCli = HashCodeHelper.Combine(methodIDFlip, branch.BranchLabel);

#if DEBUG
                    if (!branchIDMap.ContainsKey(branchIDForCli))
                    {
                        string methodName = "N/A";
                        if (branch.Method != null)
                            methodName = branch.Method.ShortName;
                        branchIDMap.Add(branchIDForCli, methodName + branch.BranchLabel);
                    }
#endif

                    if (!this.branchFitnessMap.TryGetValue(branchIDForCli, out cli))
                        this.branchFitnessMap[branchIDForCli] = cli = new BranchFitnessGain(branchIDForCli);
                    //else
                    //    this.Log.LogMessage("fitness",
                    //                     "Find a fitness gain for branch from Branch {0} for target {1} (accumulated gain: {2} / count {3})",
                    //                    branchIDForCli, targetID, cli.GetAccumulatedFitnessGain(targetID), cli.GetAccumulatedFitnessCount(targetID));


                    if (node == flippedNode)
                    {
#if DEBUG
                        this.SetFlippedPathNumberToFlippedNode(node);
#endif
                        foreach (var succ in Map.GetValues(node.Successors))
                            if (succ != lastVisitedNode)//succ is a previously explored successor node
                            {
                                //retrieve the info for the flip-from branch
                                CodeBranch flipFromBranch = succ.InCodeBranch;

                                if (flipFromBranch == null)
                                    continue;
                                int methodIDFlipFrom = 0;
                                if (flipFromBranch.Method != null)
                                    methodIDFlipFrom = flipFromBranch.Method.GlobalIndex;

                                branchIDForcliFlipFrom = HashCodeHelper.Combine(methodIDFlipFrom, flipFromBranch.BranchLabel);

#if DEBUG
                                if (!branchIDMap.ContainsKey(branchIDForcliFlipFrom))
                                {
                                    string methodName = "N/A";
                                    if (flipFromBranch.Method != null)
                                        methodName = flipFromBranch.Method.ShortName;
                                    branchIDMap.Add(branchIDForcliFlipFrom, methodName + flipFromBranch.BranchLabel);
                                }
#endif
                                if (!this.branchFitnessMap.TryGetValue(branchIDForcliFlipFrom, out cliFlipFrom))
                                    this.branchFitnessMap[branchIDForcliFlipFrom] = cliFlipFrom = new BranchFitnessGain(branchIDForcliFlipFrom);

                                int otherFitness = this.GetFitness(succ, targetID);

                                //below calcuate the difference in the actual fitness calculated from the fitness function 
                                //note that we shouldn't use the computed fitness value after considering branch fitness gain
                                int diff;
                                if ((otherFitness == int.MaxValue) && (pathFitnessValue != int.MaxValue))
                                //if the path being flipped from does not reach the target 
                                //(covering the other side of the target) but now it reaches the target
                                {
                                    diff = pathFitnessValue;
                                }
                                else if ((pathFitnessValue == int.MaxValue) && (otherFitness != int.MaxValue))
                                //if the path being flipped from does reach the target 
                                //(covering the other side of the target) but now it does not reach the target
                                {
                                    diff = -otherFitness;
                                }
                                else
                                    diff = otherFitness - pathFitnessValue;

                                //We decide not to put penalty there since the average would take that into account

                                SetFitnessGainToFlippedNode(node, targetID, pathFitnessValue);//attached fitness gain to the flipped node, debugging use

                                if (this.isLoggingEnabled)
                                {
                                    this.Log.LogMessage("fitness",
                                             "================\n            Flipped node {0} (target: {6}) (From Branch {1} to Branch {2})'s improved fitness of {3}: {4}-{5}: real original fitness {7}",
                                            node, branchIDForcliFlipFrom, branchIDForCli, diff, otherFitness, pathFitnessValue, targetID, this.GetFitness(succ, targetID));
                                }
                                //below update the fitness gain/loss of the flip-to node in the current path
                                cli.AddFitnessGain(targetID, diff);
                                //this.Log.LogMessage("fitness",
                                //         "================\n            Flipped node {0} (target: {6}) (From Branch {1} to Branch {2})'s improved fitness of {3}: {4}-{5}: real original fitness {7}",
                                //        node, branchIDForcliFlipFrom, branchIDForCli, diff, otherFitness, pathFitnessValue, targetID, this.GetFitness(succ, targetID));


                                //this.Log.LogMessage("fitness",
                                //    "accumulated fitness of {0}: {1}/{2}",
                                //    branch, cli.GetAccumulatedFitnessGain(targetID), cli.GetAccumulatedFitnessCount(targetID));

                                //below update the fitness loss/gain of the flip-from node in a previous path                                
                                cliFlipFrom.AddFitnessGain(targetID, -diff);

                                //this.Log.LogMessage("fitness",
                                //    "accumulated fitness of {0}: {1}/{2}",
                                //    flipFromBranch, cliFlipFrom.GetAccumulatedFitnessGain(targetID), cliFlipFrom.GetAccumulatedFitnessCount(targetID));
                            }

                    }
                    int fitnessGainForBranch = cli.GetAverageFitnessGain(targetID);
                    //this.Log.LogMessage("fitness",
                    //    "Get fitness gain of branch {0}: {1} for target {2} (accumulated gain: {3} / count {4})",
                    //    branchIDForCli, fitnessGainForBranch, targetID, cli.GetAccumulatedFitnessGain(targetID), cli.GetAccumulatedFitnessCount(targetID));
                    
                    if (!SetFitnessValueToNode(targetsImprovedInThisPath, flippedNode, node, targetID, pathFitnessValue, fitnessGainForBranch, cli.BranchID))
                        break;
                }

                lastVisitedNode = node;
            }
        }

        public void SetCoveredTarget(IExecutionNode flippedNode, int targetID)
        {
            SafeDebug.AssumeNotNull(flippedNode, "flippedNode");
            int nodeId = flippedNode.UniqueIndex;
            TargetFitnessInfo targetFitness;
            if (!this.nodeFitnessMap.TryGetValue(nodeId, out targetFitness))
            {
                targetFitness = new TargetFitnessInfo(this, nodeId);
                nodeFitnessMap.Add(nodeId, targetFitness);
            }
            targetFitness.AddCoveratedTargets(targetID);
        }

#if DEBUG
        void SetFlippedPathNumberToFlippedNode(IExecutionNode node)
        {
            TargetFitnessInfo targetFitness;
            if (this.nodeFitnessMap.TryGetValue(node.UniqueIndex, out targetFitness))
            {
                targetFitness.SetFlippedRunNumber(this.currentPathNumber-1, TargetIDOfPrecedingFrontier, FitnessValueOfPrecedingFrontier, PriorityOfTheChosenTargetInFrontier);
            }
        }
#endif

        public void SetFitnessGainToFlippedNode(IExecutionNode node, int targetID, int pathFitnessValue)
        {
            int oldFitness;
            TargetFitnessInfo targetFitness;
            if (!this.nodeFitnessMap.TryGetValue(node.UniqueIndex, out targetFitness))
            {
                targetFitness = new TargetFitnessInfo(this, node.UniqueIndex);
                this.nodeFitnessMap.Add(node.UniqueIndex, targetFitness);
                oldFitness = int.MaxValue;
            }
            else
                oldFitness = targetFitness.GetFitnessValue(targetID);

#if DEBUG
            int fitnessValueGain = oldFitness - pathFitnessValue;
            targetFitness.SetFitnessGainForCurrentNodeFlipping(targetID, fitnessValueGain);
#endif
        }

        public bool SetFitnessValueToNode(SafeSet<int> targetsImprovedInThisPath, IExecutionNode flippedNode, IExecutionNode node, int targetID, int pathFitnessValue, int targetFitnessGain, int branchID)
        {
            int oldFitness;
            TargetFitnessInfo targetFitness;
            if (!this.nodeFitnessMap.TryGetValue(node.UniqueIndex, out targetFitness))
            {
                targetFitness = new TargetFitnessInfo(this, node.UniqueIndex);
                this.nodeFitnessMap.Add(node.UniqueIndex, targetFitness);
                oldFitness = int.MaxValue;
            }
            else
                oldFitness = targetFitness.GetFitnessValue(targetID);

            if (pathFitnessValue < oldFitness)
            {
                targetFitness.SetFitnessValue(targetID, pathFitnessValue, targetNodeMap, targetFitnessGain, branchID);
                //this.Log.LogMessage("fitness",
                //    "set fitness value {0} (old: {1}): branch gain: {2}  for \n            node {3} (target: {4}): branch id: {5}",
                //    pathFitnessValue, oldFitness, targetFitnessGain, node, targetID, branchID);
                RemoteEventHandler<PexFitnessEventArgs> eh = this.OnFitness;
                if (eh != null)
                    eh(new PexFitnessEventArgs(flippedNode, node, targetID));

                updateGlobalFitnessForTarget(targetsImprovedInThisPath, flippedNode, targetID, targetFitness.GetFitnessValue(targetID));

                return true;
            }
            else
            {
                /*
                this.Log.LogMessage("fitness",
                    "Not improving fitness value {0} (old: {1}): branch gain: {2}  for \n            node {3} (target: {4}): branch id: {5}",
                    pathFitnessValue, oldFitness, targetFitnessGain, node, targetID, branchID);

                */
                return false;
            }

        }

        public int GetFitness(IExecutionNode node, int targetID)
        {
            TargetFitnessInfo targetFitness;
            if (!this.nodeFitnessMap.TryGetValue(node.UniqueIndex, out targetFitness))
                return int.MaxValue;//if the fitness value doesn't exist, return max int value
            else
                return targetFitness.GetFitnessValue(targetID);
        }

        //note that if we ask for the fitness value of a node without giving target id
        //then we return the min fitness value for all the targets for the node
        //the return value may not be meaningful when the strategy is 
        //not StrategyKind.OverallMinFitnessValueForAllTargets
        public int GetComputedFitness(IExecutionNode node)
        {
            TargetFitnessInfo targetFitness;
            if (!this.nodeFitnessMap.TryGetValue(node.UniqueIndex, out targetFitness))
                return TargetFitnessInfo.DefaultMinPexCompositeFitnessValue;
            else
                return targetFitness.MinPexCompositeFitnessValue;
        }

        public IFiniteMap<int, PexCompositeFitnessValue> GetTargetFitnessInfo(IExecutionNode node)
        {
            TargetFitnessInfo targetFitness;
            if (!this.nodeFitnessMap.TryGetValue(node.UniqueIndex, out targetFitness))
                return Map.Empty<int, PexCompositeFitnessValue>();
            else
                return targetFitness.TargetCompositeFitnessMap;
        }

#if DEBUG
        public string GetTargetIDString(int target)
        {
            string idStr;
            if (this.TargetIDMap.TryGetValue(target, out idStr))
                return idStr;
            else
                return String.Empty;
        }

        public string GetBranchIDString(int branch)
        {
            string idStr;
            if (this.branchIDMap.TryGetValue(branch, out idStr))
                return idStr;
            else
                return String.Empty;
        }

        public string GetIDMapString()
        {
            var sb = new SafeStringBuilder();
            sb.Append("Target ID Map\n");
            foreach (var kvp in TargetIDMap)
                sb.Append(" Target: " + kvp.Key + ":" + kvp.Value);
            sb.Append("\n Branch ID Map\n");
            foreach (var kvp in this.branchIDMap)
                sb.Append(" Branch: " + kvp.Key + ":" + kvp.Value);

            foreach (int key in targetNodeMap.Keys)
            {
                if (!this.HasCoveredTarget(key))
                    sb.Append(" Uncovered Target: " + key + ":" + TargetIDMap[key]);
            }

            return sb.ToString();
        }
#endif

        const bool noRepresentationForUnFlippedNodes = true;//if false, all nodes' fitness info will be shown

        //used for debugging, the method GetCompositeFitnessRepresentation below is invoked for each node 
        //when a graph is generated in the end of all path explorations. Then if it is first invoked,
        //we output the map of target id and branch id info for debugging 
        bool isFirstTime = true;
        public string GetCompositeFitnessRepresentation(IExecutionNode node)
        {
#if DEBUG
            if (isFirstTime)
            {
                isFirstTime = false;
                //if (logging)
                //{
                this.Log.LogMessage("fitness", "{0}", GetIDMapString());
                //}
            }
#endif
            bool flipped = false;
            TargetFitnessInfo targetFitness;
            if (this.nodeFitnessMap.TryGetValue(node.UniqueIndex, out targetFitness))
            {
                var sb = new SafeStringBuilder();
                sb.Append("Branch:" + targetFitness.BranchID + "\n");
#if DEBUG
                if (targetFitness.flippedPathNumber == 0)
                    sb.Append("Flipped run: NO Creation run:" + targetFitness.firstEncounteredPathNumber + "\n");
                else
                    sb.Append("Flipped run: " + targetFitness.flippedPathNumber + " Creation run:" + targetFitness.firstEncounteredPathNumber + "\n");

                if (targetFitness.TargetIDOfFlipping == 0)
                    sb.Append("Flipped for target N/A with fitness " + targetFitness.FitnessValueOfFlipping + "\n");
                else
                {
                    sb.Append("Flipped for target " + targetFitness.TargetIDOfFlipping + " priority: " + targetFitness.PriorityOfTargetOfFlipping + " fitness: " + targetFitness.FitnessValueOfFlipping + "\n");
                    flipped = true;
                }

                foreach (var kvp in targetFitness.FitnessGainForTargetOfFlipping)
                {
                    int targetID = kvp.Key;
                    int fitnessGain = kvp.Value;

                    if (fitnessGain != 0)
                        sb.Append("Flipped to cause target " + targetID + " to gain fitness " + fitnessGain + "\n");
                }
#endif
                foreach (int coveredTargetID in targetFitness.CoveredTargets)
                {
                    sb.Append("Covered target:" + coveredTargetID + "\n");
                }

                foreach (var kvp in targetFitness.TargetCompositeFitnessMap)
                {
                    var targetID = kvp.Key;
                    PexCompositeFitnessValue compositFitnessValue = kvp.Value;
                    sb.Append("Target:" + targetID + " ");
                    sb.Append(compositFitnessValue.ToString());
                    sb.Append("\n");
                }

                if (!flipped && noRepresentationForUnFlippedNodes)
                    return "FIT: unflipped";
                else
                    return sb.ToString();
            }
            else
                return "FIT:unfound";
        }

        public event RemoteEventHandler<PexFitnessEventArgs> OnFitness;
        public event RemoteEventHandler<PexFitnessEventArgs> OnTargetCoverage;
        public event RemoteEventHandler<PexFitnessEventArgs> OnTargetFitnessImprovement;

        public void SendEventOnTargetCoverage(IExecutionNode flippedNode, int targetID)
        {
            var eh = this.OnTargetCoverage;
            if (eh != null)
                eh(new PexFitnessEventArgs(flippedNode, null, targetID));
        }

        //below is used to keep track of those predicates that involve non-boolean values, i.e., values other
        //than 1 or 0. Then we can later determine whether a predicate is a boolean predicate or not
        //if it is, we don't keep track of it for fitness
        SafeSet<int> reachedNonBooleanComparisonHashes = new SafeSet<int>();
        public void ReachedNonBooleanComparison(MethodDefinition method, int programCounter)
        {
            SafeDebug.AssumeNotNull(method, "method");
            int hc = HashCodeHelper.Combine(method.GlobalIndex, programCounter);
            this.reachedNonBooleanComparisonHashes.Add(hc);
        }

        public bool IsReachedNonBooleanComparison(MethodDefinition method, int programCounter)
        {
            SafeDebug.AssumeNotNull(method, "method");
            int hc = HashCodeHelper.Combine(method.GlobalIndex, programCounter);
            return this.reachedNonBooleanComparisonHashes.Contains(hc);
        }

        #endregion
    }
}

